Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    app(app(map,f),nil)  → nil
2:    app(app(map,f),app(app(cons,x),xs))  → app(app(cons,app(f,x)),app(app(map,f),xs))
3:    app(app(append,xs),nil)  → xs
4:    app(app(append,nil),ys)  → ys
5:    app(app(append,app(app(cons,x),xs)),ys)  → app(app(cons,x),app(app(append,xs),ys))
6:    app(app(zip,nil),yss)  → yss
7:    app(app(zip,xss),nil)  → xss
8:    app(app(zip,app(app(cons,xs),xss)),app(app(cons,ys),yss))  → app(app(cons,app(app(append,xs),ys)),app(app(zip,xss),yss))
9:    app(app(combine,xs),nil)  → xs
10:    app(app(combine,xs),app(app(cons,ys),yss))  → app(app(combine,app(app(zip,xs),ys)),yss)
11:    app(levels,app(app(node,x),xs))  → app(app(cons,app(app(cons,x),nil)),app(app(combine,nil),app(app(map,levels),xs)))
There are 25 dependency pairs:
12:    APP(app(map,f),app(app(cons,x),xs))  → APP(app(cons,app(f,x)),app(app(map,f),xs))
13:    APP(app(map,f),app(app(cons,x),xs))  → APP(cons,app(f,x))
14:    APP(app(map,f),app(app(cons,x),xs))  → APP(f,x)
15:    APP(app(map,f),app(app(cons,x),xs))  → APP(app(map,f),xs)
16:    APP(app(append,app(app(cons,x),xs)),ys)  → APP(app(cons,x),app(app(append,xs),ys))
17:    APP(app(append,app(app(cons,x),xs)),ys)  → APP(app(append,xs),ys)
18:    APP(app(append,app(app(cons,x),xs)),ys)  → APP(append,xs)
19:    APP(app(zip,app(app(cons,xs),xss)),app(app(cons,ys),yss))  → APP(app(cons,app(app(append,xs),ys)),app(app(zip,xss),yss))
20:    APP(app(zip,app(app(cons,xs),xss)),app(app(cons,ys),yss))  → APP(cons,app(app(append,xs),ys))
21:    APP(app(zip,app(app(cons,xs),xss)),app(app(cons,ys),yss))  → APP(app(append,xs),ys)
22:    APP(app(zip,app(app(cons,xs),xss)),app(app(cons,ys),yss))  → APP(append,xs)
23:    APP(app(zip,app(app(cons,xs),xss)),app(app(cons,ys),yss))  → APP(app(zip,xss),yss)
24:    APP(app(zip,app(app(cons,xs),xss)),app(app(cons,ys),yss))  → APP(zip,xss)
25:    APP(app(combine,xs),app(app(cons,ys),yss))  → APP(app(combine,app(app(zip,xs),ys)),yss)
26:    APP(app(combine,xs),app(app(cons,ys),yss))  → APP(combine,app(app(zip,xs),ys))
27:    APP(app(combine,xs),app(app(cons,ys),yss))  → APP(app(zip,xs),ys)
28:    APP(app(combine,xs),app(app(cons,ys),yss))  → APP(zip,xs)
29:    APP(levels,app(app(node,x),xs))  → APP(app(cons,app(app(cons,x),nil)),app(app(combine,nil),app(app(map,levels),xs)))
30:    APP(levels,app(app(node,x),xs))  → APP(cons,app(app(cons,x),nil))
31:    APP(levels,app(app(node,x),xs))  → APP(app(cons,x),nil)
32:    APP(levels,app(app(node,x),xs))  → APP(cons,x)
33:    APP(levels,app(app(node,x),xs))  → APP(app(combine,nil),app(app(map,levels),xs))
34:    APP(levels,app(app(node,x),xs))  → APP(combine,nil)
35:    APP(levels,app(app(node,x),xs))  → APP(app(map,levels),xs)
36:    APP(levels,app(app(node,x),xs))  → APP(map,levels)
The approximated dependency graph contains one SCC: {12,14-17,19,21,23,25,27,29,31,33,35}.
Tyrolean Termination Tool  (53.05 seconds)   ---  May 4, 2006